\begin{tabbing}
FairFifo
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=($\forall$$i$:Id, $t$:$\mathbb{N}$, $l$:IdLnk. ($\neg$(source($l$) = $i$)) $\Rightarrow$ (onlnk($l$;m($i$;$t$)) = []))\+
\\[0ex]\& (\=$\forall$$i$:Id, $t$:$\mathbb{N}$.\+
\\[0ex]($\uparrow$isnull(a($i$;$t$))) $\Rightarrow$ (($\forall$$x$:Id. s($i$;$t$+1).$x$ = ($\lambda$$q$.s($i$;$t$).$x$($q$ + 1))) \& m($i$;$t$) = []))
\-\\[0ex]\& (\=($\forall$$i$:Id, $t$:$\mathbb{N}$, $l$:IdLnk.\+
\\[0ex]($\uparrow$isrcv($l$;a($i$;$t$)))
\\[0ex]$\Rightarrow$ \=(destination($l$) = $i$\+
\\[0ex]\& (($\parallel$queue($l$;$t$)$\parallel$ $\geq$ 1 ) c$\wedge$ (hd(queue($l$;$t$)) = msg(a($i$;$t$))))))
\-\\[0ex]c$\wedge$ \=((\=$\forall$$l$:IdLnk, $t$:$\mathbb{N}$.\+\+
\\[0ex]$\exists$${\it t'}$:$\mathbb{N}$. (($t$ $\leq$ ${\it t'}$) \& (($\uparrow$isrcv($l$;a(destination($l$);${\it t'}$))) $\vee$ (queue($l$;${\it t'}$) = []))))
\-\\[0ex]\& w{-}machine{-}constraint($w$)
\\[0ex]\& w{-}atom{-}constraint($w$)
\\[0ex]\& w{-}discrete{-}constraint($w$)))
\-\-\-
\end{tabbing}